Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this problem (...) by applying recent methods from sorted logics. This paper presents a resolution calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)

Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using a three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this (...) problem by applying recent methods from sorted logics. This paper presents a tableau calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)

(2012). Reasoning without believing: on the mechanisation of presuppositions and partiality. Journal of Applied Non-Classical Logics: Vol. 22, No. 4, pp. 295-317. doi: 10.1080/11663081.2012.705962.

Since Mathematics really is about what mathematicians do, in this paper, we will look at the mathematical practice of framing , in which an object of interest is viewed in terms of well-understood mathematical structures. The new perspective not only allows to deepen the understanding of e resp. object, it also facilitates new insights. We propose a model for framing in the context of theory graphs, and show how framing can be exploited to enhance the interaction with MKM systems. We (...) use the framing extension of our SACHS system — a semantic help system for MS Excel — as a concrete example. (shrink)

The interest of the field of Mathematical Knowledge Management is predicated on the assumption that by investing into markup or formalization of mathematical knowledge, we can reap benefits in managing (creating, classifying, reusing, verifying, and finding) mathematical theories, statements, and objects. This global value proposition has been used to motivate the pursuit of technologies that can add machine support to these knowledge management tasks. But this (rather naive) technology-centered motivation takes a view merely from the global (macro) perspective, and almost (...) totally disregards the user’s point of view and motivations for using it, the local (micro) perspective. In this paper we go a first step into a more principled analysis of the MKM value proposition by focusing on motivations for mathematical search engines from the micro perspective. We will use a table-based method called the “Added-Value Analysis” (AVA) developed by one of the authors. Even though we apply the AVA only to mathematical search engines, the method quickly leads to value considerations that are relevant for the whole field of MKM. (shrink)

Der vorliegende dritte Band der Briefedition dokumentiert den Briefwechsel der Jahre 1734 und 1735. Mit seiner Ernennung zum Professor für Logik und Metaphysik und seiner Heirat mit Luise Adelgunde Victorie Kulmus ist Gottsched Mitte der 1730er Jahre in Leipzig fest etabliert. Die Briefe bieten wichtige Einblicke in die Entwicklung der von ihm geleiteten Deutschen Gesellschaft (vor allem zu dem von ihr herausgegebenen ersten Periodikum zur Literaturwissenschaft), in die Aufnahme und Wirkung seiner Werke, u.a. der Theaterstücke, und in seine Übersetzertätigkeit. Sie (...) sind daneben eine hervorragende Quelle für Studienbetrieb und Studentenleben des 18. Jahrhunderts. (shrink)

Bd. 1. Lebensbeschreibungen und Dokumente -- Bd. 2. Kommentar.

In this contribution we propose an agent architecture for theorem proving which we intend to investigate in depth in the future. The work reported in this paper is in an early state, and by no means finished. We present and discuss our proposal in order to get feedback from the Calculemus community.

In this paper we present an approach to automated learning within mathematical reasoning systems. In particular, the approach enables proof planning systems to automatically learn new proof methods from well-chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our approach consists of an abstract representation for methods and a machine learning technique which can learn methods using this representation formalism. We present an implementation of the approach within the ΩMEGA proof planning system, which we call (...) LEARNΩMATIC. We also present the results of the experiments that we ran on this implementation in order to evaluate if and how it improves the power of proof planning systems. (shrink)

The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.

In this paper, we show that Higher{Order Coloured Uni cation { a form of uni cation developed for automated theorem proving { provides a general theory for modeling the interface between the interpretation process and other sources of linguistic, non semantic information. In particular, it provides the general theory for the Primary Occurrence Restriction which (Dalrymple et al., 1991)'s analysis called for.

The history of building automated theorem provers for higher-order logic is almost as old as the field of deduction systems itself. The first successful attempts to mechanize and implement higher-order logic were those of Huet [13] and Jensen and Pietrzykowski [17]. They combine the resolution principle for higher-order logic (first studied in [1]) with higher-order unification. The unification problem in typed λ-calculi is much more complex than that for first-order terms, since it has to take the theory of αβη-equality into (...) account. As a consequence, the higher-order unification problem is undecidable and sets of solutions need not even always have most general elements that represent them. Thus the mentioned calculi for higher-order logic have take special measures to circumvent the problems posed by the theoretical complexity of higher-order unification. In this paper, we will exemplify the methods and proof- and model-theoretic tools needed for extending first-order automated theorem proving to higherorder logic. For the sake of simplicity take the tableau method as a basis (for a general introduction to first-order tableaux see part I.1) and discuss the higherorder tableau calculi HT and HTE first presented in [19]. The methods in this paper also apply to higher-order resolution calculi [1, 13, 6] or the higher-order matings method of Peter [3], which extend their first-order counterparts in much the same way. Since higher-order calculi cannot be complete for the standard semantics by Gödel’s incompleteness theorem [11], only the weaker notion of Henkin models [12] leads to a meaningful notion of completeness in higher-order logic. It turns out that the calculi in [1, 13, 3, 19] are not Henkin-complete, since they fail to capture the extensionality principles of higher-order logic. We will characterize the deductive power of our calculus HT (which is roughly equivalent to these calculi) by the semantics of functional Σ-models. To arrive at a calculus that is complete with respect to Henkin models, we build on ideas from [6] and augment HT with tableau construction rules that use the extensionality principles in a goal-oriented way.. (shrink)

Both Higher-Order Uni cation approaches to In linguistic theories on discourse coherence Kehler, discourse semantics Dalrymple et al., 1991; Shieber et.

Sequences play a great role in mathematical communication. In mathematical notation, we use sequence ellipsis (. . . ) to denote "obvious" sequences like 1, 2, . . . , 7, and in conceptualizations sequence constructors like (i 2+1) i∈N. Furthermore, sequences have a prominent role as argument sequences of flexary functions. While the former cases can adequately be represented and reasoned about as domain objects in Open- Math and MathML, argument sequences are at the language level, and can only (...) be represented, but not reasoned with, since the necessary (sequence-schematic) axioms cannot be represented in the language. (shrink)

We present a content markup language for physics realized by extending the OMDoc format by an infrastructure for the principal concepts of physics: observables, physical systems, and experiments.

We explore the social context of mathematical knowledge: Even though, the community of mathematicians may look homogeneous from the outside, it is actually structured into various sub-communities that differ in preferred notations, the choice of basic assumptions, or e.g. in the choice of motivating examples. We contend that we cannot manage mathematical knowledge for human recipients if we do not take these factors into account. As a basis for a future extension of MKM systems, we analyze the social context of (...) information in terms of Communities of Practice (CoP; a concept from learning theory) and present a concrete extensional model for CoPs in mathematics. (shrink)

Spreadsheets are mathematical documents that are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. In this paper we show that spreadsheets are interesting applications for MKM techniques which can alleviate usability and maintenance problems as spreadsheet-based applications grow evermore complex and longlived. We present the software and information architecture of a semantic enhancement of MS Excel spreadsheets that aims at compensating the computational bias in spreadsheets.

The effort to align MathML 3 and OpenMath has led to a realisation that (pragmatic) MathML’s condition and domainofapplication elements, when used with quantifiers, do not have a neat expression in OpenMath. This paper analyzes the situation focusing on quantifiers and proposes a solution, via six new symbols. Two of them fit completely within the existing OpenMath structure, and we place them in the associated quant3 CD. The others require a generalization of OMBIND. We also propose, logically separately but in (...) the same area, a quant2 CD with existsuniquely, commonly written ∃!, and the ‘fusion’ symbol existsuniquelyin. In a second step we generalize the solution to the phenomenon of big operators that MathML 2 implicitly provides but which do not have a direct counterpart in the OpenMath CDs. (shrink)

One of the fundamental and seemingly simple aims of mathematical knowledge management (MKM) is to develop and standardize formats that allow to “represent the meaning of the objects of mathematics”. The open formats OpenMath and MathML address this, but differ subtly in syntax, rigor, and structural viewpoints (notably over calculus). To avoid fragmentation and smooth out interoperability obstacles, effort is under way to align them into a joint format OpenMath/MathML 3. We illustrate the issues that come up in such an (...) alignment by looking at three main areas: bound variables and conditions, calculus (which relates to the previous) and “lifted” n-ary operators. (shrink)

Semantic analysis, – inference on the basis of semantic information and world knowledge – still is largely uncharted territory in dy- (3) namic semantics. It is needed, among other things, for the reconstruction of linguistically unspecified parts of the discourse or for restricting ambiguities introduced by prior analysis processes, i.e.

Notations are central for understanding mathematical discourse. Readers would like to read notations that transport the meaning well and prefer notations that are familiar to them. Therefore, authors optimize the choice of notations with respect to these two criteria, while at the same time trying to remain consistent over the document and their own prior publications. In print media where notations are fixed at publication time, this is an over-constrained problem. In living documents notations can be adapted at reading time, (...) taking reader preferences into account. We present a representational infrastructure for notations in living mathematical documents. Mathematical notations can be defined declaratively. Author and reader can extensionally define the set of available notation definitions at arbitrary document levels, and they can guide the notation selection function via intensional annotations. We give an abstract specification of notation definitions and the flexible rendering algorithms and show their coverage on paradigmatic examples. We show how to use this framework to render OpenMath and Content-MathML to Presentation-MathML, but the approach extends to arbitrary content and presentation formats. We discuss prototypical implementations of all aspects of the rendering pipeline. (shrink)

Michael Kohlhase and Mandy Simons. Interpreting Negatives in Discourse.

ABSTRACT This paper introduces a multi-valued variant of higher-order resolution and proves it correct and complete with respect to a variant of Henkin's general model semantics. This resolution method is parametric in the number of truth values as well as in the particular choice of the set of connectives (given by arbitrary truth tables) and even substitutional quantifiers. In the course of the completeness proof we establish a model existence theorem for this logical system. The work reported in this paper (...) provides a basis for developing higher-order mechanizations for many non-classical logics. (shrink)

Spreadsheets are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. In previous work we have studied how an explicit representation of the background knowledge associated with the spreadsheet can be exploited to alleviate usability problems with spreadsheet-based applications. The SACHS system implements this approach to provide a semantic help system for DCS, an Excelbased financial controlling system.

MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM “in the small” is well-studied, so the real problem is to scale up to large, highly interconnected corpora: “MKM in the large”. We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need software architectures and implementations that implement these operations scalably on large knowledge bases. We present instances (...) of both in this paper: the MMT framework for modular theory-graphs that integrates meta-logical foundations, which forms the base of the next OMDOC version; and TNTBase, a versioned storage system for XML- based document formats. TNTBase becomes an MMT database by instantiating it with special MKM operations for MMT. (shrink)

This paper introduces the concept of Virtual Documents and its prototypical realization in our TNTBase system, a versioned XML database. VDs integrate XQuery-based computational facilities into documents like JSP/PHP do for relational queries. We view the integration of computation in documents as an enabling technology and evaluate it on a handfull of real-world use cases.

The semantics of everyday language and the semantics..

We describe an experiment of transforming large collections of L ATEX documents to more machine-understandable representations. Concretely, we are translating the collection of scientific publications of..

The Analytica system is a theorem proving system for 19 th century mathematics written on top of the Mathematica computer algebra system. It was developed in the early 1990’s by X. Zhao and E. Clarke and has since been dormant. We describe recent work to resurrect the theorem prover and port it to newer versions of Mathematica. The new system Analytica 2 can still prove the same theorems, but has been significantly cleaned up. The code has been restructured and documented, (...) the declarative knowledge has been separated from a logical kernel, and the system is being made available as a MathWeb service. (shrink)

We present a search engine for mathematical formulae. The MathWebSearch system harvests the web for content representations (currently MathML and OpenMath) of formulae and indexes them with substitution tree indexing, a technique originally developed for accessing intermediate results in automated theorem provers. For querying, we present a generic language extension approach that allows constructing queries by minimally annotating existing representations. First experiments show that this architecture results in a scalable application.

This package provides an infrastructure for semantically enhanced requirements specifications used in software engineering. This allows to embed structural information into documents that can be used by semantic document managment systems e.g. for management of change and requirements tracing.

Although knowledge is a central topic for MKM there is little explicit discussion on what ‘knowledge’ might actually be. There are specific intuitions about form and content of knowledge, about its structure, and epistemological nature that shape the MKM systems, but a conceptual model is missing. In this paper we try to rationalize this discussion to give MKM a firmer footing, to start a discussion among MKM researchers and help relate the MKM intuitions and discourses to other communities. Starting from (...) the observation that many concrete realizations of mathematical knowledge objects are considered equivalent, we propose a conceptual model of the space of (mathematical) knowledge objects graded by levels of abstraction and presentational explicitness and draw conclusions for MKM markup formats. (shrink)

Thus, despite the di culty of higher-order automated theorem proving, which has to deal with problems like the undecidability of higher-order uni - cation (HOU) and the need for primitive substitution, there are proof problems which lie beyond the capabilities of rst-order theorem provers, but instead can be solved easily by an higher-order theorem prover (HOATP) like Leo. This is due to the expressiveness of higher-order Logic and, in the special case of Leo, due to an appropriate handling of the (...) extensionality principles (functional extensionality and extensionality on truth values). (shrink)

In the last two decades, the World Wide Web has become the universal, and — for many users — main information source. Search engines can efficiently serve daily life information needs due to the enormous redundancy of relevant resources on the web. For educational — and even more so for scientific information needs, the web functions much less efficiently: Scientific publishing is built on a culture of unique reference publications, and moreover abounds with specialized structures, such as technical nomenclature, notational (...) conventions, references, tables, or graphs. Moreover, many of these structures are peculiar to specialized communities determined by nationality, research group membership, or adherence to a special school of thought. To keep the much-lamented “digital divide” from becoming a “cultural divide”, we have to make online material more accessible and adaptable to individual users. In this paper we attack this goal for the field of mathematics where knowledge is abstract, highly structured, and extraordinarily interlinked. Modern, content-based representation formats like OpenMath or content MathML allow us to capture, model, relate, and represent mathematical knowledge objects and thus make them context-aware and machine-adaptable to the respective user contexts. Building on previous work which can make mathematical notations adaptable we employ user modeling techniques to make them adaptive to relieve the reader of configuration tasks. We present a comprehensive framework for adaptive notation management and evaluate it on an implementation integrated in the e-learning platform panta rhei. (shrink)